/*
 * Configuration.cpp
 *
 *  Created on: Apr 30, 2012
 *      Author: kobe
 */

#include "Configuration.h"
#include <cstdio>

Configuration::Configuration(Sequent* s, std::vector<Rule*>* r) {
	this->mSequent = new Sequent(s->toString());
	this->mAvailableRule = new std::vector<Rule*>;
	this->mSubConfiguration = new std::vector<Configuration*>;
	for (size_t i = 0; i < r->size(); i++) {
		mAvailableRule->push_back(r->at(i));
	}
	this->mIsProofTreeLeaf = false;
	this->mParent = NULL;
}

Configuration::~Configuration() {
	// TODO Auto-generated destructor stub
}

void Configuration::setParent(Configuration* parent) {
	mParent = parent;
}

bool Configuration::prove() {
	A_Id* id = new A_Id;
	A_TopR* top = new A_TopR;
	A_BottomL* bot = new A_BottomL;
	if (id->test(*mSequent)) {
		mAxiom = id;
		mIsProofTreeLeaf = true;
		return true;
	}
	if (top->test(*mSequent)) {
		mAxiom = top;
		mIsProofTreeLeaf = true;
		return true;
	}
	if (bot->test(*mSequent)) {
		mAxiom = bot;
		mIsProofTreeLeaf = true;
		return true;
	}
	for (size_t i = 0; i < mAvailableRule->size(); i++) {
		this->mRule = mAvailableRule->at(i);
		//std::cout << mRule->toString() << std::endl;
		std::vector<Sequent*> result;
		size_t numOfRun = 1;
		Various_Rule: if (mRule->isVariousRule()) {
			result = ((VariousRule*) mRule)->run(mSequent, numOfRun);
		} else {
			result = mRule->run(mSequent);
		}
		//std::cout << "Result no of sequent:" << result.size() << std::endl;
		bool right_rule = true;
		if (result.size() <= 0) {
			right_rule = false;
		}
		for (size_t j = 0; j < result.size(); j++) {
			if (!checkLoop(result[j])) {
//				std::cout << mRule->toString() << std::endl;
//				std::cout << result[j]->toString() << std::endl;
//				std::cout << result[j]->toLatex() << std::endl;
//				std::cout << "Press any key to continue..." << std::endl;
//				int ch = getchar();
				Configuration* c = new Configuration(result[j], mAvailableRule);
				c->setParent(this);
				mSubConfiguration->push_back(c);
				if (!c->prove()) {
					right_rule = false;
				}
			} else {
				right_rule = false;
			}
		}
		if (right_rule) {
			return true;
		}

		//current rule has multiple possible results
		if (result.size() > 0 && mRule->isVariousRule()) {
			std::cout << "num of run:" << numOfRun << std::endl;
			numOfRun++;
			goto Various_Rule;
		}

		//current rule can run into loops
		if (mRule->isLoopRule()) {
			mRule->popLastSequent();
		}

		mSubConfiguration->clear();
	}
	return false;
}

std::string Configuration::toLatex() {
	std::string s("\n\\infer");
	s += "[";
	if (mIsProofTreeLeaf) {
		if (mAxiom != NULL)
			s += mAxiom->toLatex();
	} else {
		if (mRule != NULL)
			s += mRule->toLatex();
	}
	s += "]";
	s += "{";
	//bottom sequent
	if (mSequent != NULL)
		s += mSequent->toLatex();
	s += "}";
	s += "{";
	//top sequent
	if (!mIsProofTreeLeaf && mSubConfiguration->size() > 0) {
		for (size_t i = 0; i < mSubConfiguration->size() - 1; i++) {
			s += mSubConfiguration->at(i)->toLatex();
			s += "\\;";
		}
		s += mSubConfiguration->back()->toLatex();
	}
	s += "}";
	return s;
}

Sequent* Configuration::getSequent() {
	return mSequent;
}

Configuration* Configuration::getParent() {
	return mParent;
}

bool Configuration::checkLoop(Sequent* sequent) {
	Configuration *c = mParent;
	Configuration *parent = c;
	while (c != NULL) {
		if (sequent->toString().compare(c->getSequent()->toString()) == 0) {
			return true;
		}
		parent = c;
		c = c->getParent();
	}

	if (parent != NULL) {
		std::cout << "\n******************************************************" << std::endl;
		std::cout << parent->toLatex() << std::endl;
	}

	Context *context = sequent->getContext();
	std::vector<Context*> items = context->getItemList();
	if (items.size() > 1) {
		Context *c0 = items[0];
		size_t counter = 0;
		for (size_t i = 1; i < items.size(); i++) {
			if (c0->compare(items[i])) {
				counter++;
			}
			if (counter > 2) {
				return true;
			}
		}
	}
	return false;
}

